<!DOCTYPE html>
<html><head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/>
<title>test.mm</title>
<meta name="generator" content="KF5::SyntaxHighlighting - Definition (Metamath) - Theme (Breeze Dark)"/>
</head><body style="background-color:#232629;color:#cfcfc2"><pre>
<span style="color:#7a7c7d;">$( Modified version of demo0.mm from 1-Jan-04 $)</span>

<span style="color:#7a7c7d;">$(</span>
<span style="color:#7a7c7d;">                      PUBLIC DOMAIN DEDICATION</span>

<span style="color:#7a7c7d;">This file is placed in the public domain per the Creative Commons Public</span>
<span style="color:#7a7c7d;">Domain Dedication. http://creativecommons.org/licenses/publicdomain/</span>

<span style="color:#7a7c7d;">Norman Megill - email: nm at alum.mit.edu</span>
<span style="color:#7a7c7d;">$)</span>

<span style="font-weight:bold;">$c</span><span style="color:#8e44ad;"> 0 + = -&gt; ( ) term wff |- </span><span style="font-weight:bold;">$.</span>

<span style="font-weight:bold;">$v</span><span style="color:#27aeae;"> t r s P Q </span><span style="font-weight:bold;">$.</span>

<span style="color:#da4453;">tt</span> <span style="font-weight:bold;">$f</span> <span style="color:#8e44ad;">term</span><span style="color:#27aeae;"> t </span><span style="font-weight:bold;">$.</span>
<span style="color:#da4453;">tr</span> <span style="font-weight:bold;">$f</span> <span style="color:#8e44ad;">term</span><span style="color:#27aeae;"> r </span><span style="font-weight:bold;">$.</span>
<span style="color:#da4453;">ts</span> <span style="font-weight:bold;">$f</span> <span style="color:#8e44ad;">term</span><span style="color:#27aeae;"> s </span><span style="font-weight:bold;">$.</span>
<span style="color:#da4453;">wp</span> <span style="font-weight:bold;">$f</span> <span style="color:#8e44ad;">wff</span><span style="color:#27aeae;"> P </span><span style="font-weight:bold;">$.</span>
<span style="color:#da4453;">wq</span> <span style="font-weight:bold;">$f</span> <span style="color:#8e44ad;">wff</span><span style="color:#27aeae;"> Q </span><span style="font-weight:bold;">$.</span>

<span style="color:#da4453;">tze</span> <span style="font-weight:bold;">$a</span> <span style="color:#8e44ad;">term</span><span style="color:#27aeae;"> 0 </span><span style="font-weight:bold;">$.</span>
<span style="color:#da4453;">tpl</span> <span style="font-weight:bold;">$a</span> <span style="color:#8e44ad;">term</span><span style="color:#27aeae;"> ( t + r ) </span><span style="font-weight:bold;">$.</span>

<span style="color:#da4453;">weq</span> <span style="font-weight:bold;">$a</span> <span style="color:#8e44ad;">wff</span><span style="color:#27aeae;"> t = r </span><span style="font-weight:bold;">$.</span>
<span style="color:#da4453;">wim</span> <span style="font-weight:bold;">$a</span> <span style="color:#8e44ad;">wff</span><span style="color:#27aeae;"> ( P -&gt; Q ) </span><span style="font-weight:bold;">$.</span>

<span style="color:#da4453;">a1</span> <span style="font-weight:bold;">$a</span> <span style="color:#8e44ad;">|-</span><span style="color:#27aeae;"> ( t = r -&gt; ( t = s -&gt; r = s ) ) </span><span style="font-weight:bold;">$.</span>
<span style="color:#da4453;">a2</span> <span style="font-weight:bold;">$a</span> <span style="color:#8e44ad;">|-</span><span style="color:#27aeae;"> ( t + 0 ) = t </span><span style="font-weight:bold;">$.</span>
<span style="font-weight:bold;">${</span>
    <span style="color:#7a7c7d;">$( Define the modus ponens inference rule $)</span>
    <span style="color:#da4453;">min</span> <span style="font-weight:bold;">$e</span> <span style="color:#8e44ad;">|-</span><span style="color:#27aeae;"> P </span><span style="font-weight:bold;">$.</span>
    <span style="color:#da4453;">maj</span> <span style="font-weight:bold;">$e</span> <span style="color:#8e44ad;">|-</span><span style="color:#27aeae;"> ( P -&gt; Q ) </span><span style="font-weight:bold;">$.</span>
    <span style="color:#da4453;">mp</span>  <span style="font-weight:bold;">$a</span> <span style="color:#8e44ad;">|-</span><span style="color:#27aeae;"> Q </span><span style="font-weight:bold;">$.</span>
<span style="font-weight:bold;">$}</span>

<span style="color:#da4453;">th1</span> <span style="font-weight:bold;">$p</span> <span style="color:#8e44ad;">|-</span><span style="color:#27aeae;"> t = t </span><span style="font-weight:bold;">$=</span>
<span style="color:#da4453;">    </span><span style="color:#7a7c7d;">$( Here is its proof: $)</span>
<span style="color:#da4453;">    tt tze tpl tt weq tt tt weq tt a2 tt tze tpl</span>
<span style="color:#da4453;">    tt weq tt tze tpl tt weq tt tt weq wim tt a2</span>
<span style="color:#da4453;">    tt tze tpl tt tt a1 mp mp</span>
<span style="font-weight:bold;">$.</span>
</pre></body></html>
